rcv{-}from{-}on(${\it dE}$;${\it dL}$;${\it info}$;$e$;$l$;$r$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$rcv?(${\it info}$;$r$) $\wedge_{2}$ eqof(${\it dE}$)($e$,sender(${\it info}$;$r$)) $\wedge_{2}$ eqof(${\it dL}$)($l$,link(${\it info}$;$r$))